generated at
空でない有限全順序集合には必ず(最大元|最小元)が存在する

空でない有限全順序集合には必ず最大元/最小元が存在する
2024-03-28 11:57:35 U=\varnothingの場合を考え忘れていたtakker
証明していたときには気づかなかった
以下、 [* 空でない] を追記した
証明方針
空でない有限順序集合なら有界なはず
それを足がかりに示せばいい
証明
空でない有限順序集合が有界なことを示す
任意の空でない全順序集合(U,\le)にて、
\exist n\in\N\exist\phi:[1..n]⤖U
f:A⤖B:全単射を表す
[a..b]:=[a,b]\cap\Z
あー、わかった。\forall k\le n\exist m,M\in U\forall y\in \phi[[1..k]].m\le y\le Mを数学的帰納法で示せばいいんだ
\implies\exist n\in\N\exist\phi:[1..n]⤖U.
\phi(1)\le\phi(1)\le\phi(1)
\because反射律
\iff\exist n\in\N\exist\phi:[1..n]⤖U\forall x\in\phi[[1..1]].(\phi(1)\le x\le\phi(1))
\implies\exist n\in\N\exist\phi:[1..n]⤖U\exist m,M\in\phi[[1..1]]\forall x\in\phi[[1..1]].(m\le x\le M)
\iff\exist n\in\N\exist\phi:[1..n]⤖U.P(1)
P(k):\iff(k\le n\implies\exist m,M\in\phi[[1..k]]\forall x\in\phi[[1..k]].(m\le x\le M))とした
\iff\exist n\in\N\exist\phi:[1..n]⤖U.
\begin{dcases}P(1)\\\forall k\in\N. \end{dcases}
P(k)
\implies(
k+1\le n
\iff k+1\le n\land\exist m,M\in\phi[[1..k]]\forall x\in\phi[[1..k]].(m\le x\le M)
\implies\exist m,M\in\phi[[1..k]]
\begin{dcases}\forall x\in\phi[[1..k]].(m\le x\le M)\\\phi(k+1)\le m\lor m\le\phi(k+1)\\\phi(k+1)\le M\lor M\le\phi(k+1)\end{dcases}
\because完全律
ここで完全律を使うので、空でない有限全順序集合でないと有界性を示せない
\implies\exist m,M\in\phi[[1..k]]
\begin{dcases}\forall x\in\phi[[1..k]].(m\le x\le M)\\\phi(k+1)\le m\lor m\le\phi(k+1)\le M\lor M\le\phi(k+1)\end{dcases}
\implies\exist m,M\in\phi[[1..k]]
\forall x\in\phi[[1..k]].(\phi(k+1)\le x\le M)
\lor\forall x\in\phi[[1..k+1]].(m\le x\le M)
\lor\forall x\in\phi[[1..k]].(m\le x\le \phi(k+1))
\implies\exist m,M\in\phi[[1..k]]
\forall x\in\phi[[1..k+1]].(\phi(k+1)\le x\le M)
\lor\forall x\in\phi[[1..k+1]].(m\le x\le M)
\lor\forall x\in\phi[[1..k+1]].(m\le x\le \phi(k+1))
\because反射律
\implies\exist m,M\in\phi[[1..k+1]]\forall x\in\phi[[1..k+1]].(m\le x\le M)
)
\implies P(k+1)
\implies\exist n\in\N\exist\phi:[1..n]⤖U.
\begin{dcases}P(1)\\\forall k\in\N.(P(k)\implies P(k+1)) \end{dcases}
\implies\exist n\in\N\exist\phi:[1..n]⤖U\forall k\in\N.P(k)
\implies\exist n\in\N\exist\phi:[1..n]⤖U.P(n)
\iff\exist n\in\N\exist\phi:[1..n]⤖U\exist m,M\in\phi[[1..n]]\forall x\in\phi[[1..n]].(m\le x\le M)
\iff\exist n\in\N\exist\phi:[1..n]⤖U\exist m,M\in U\forall x\in U.(m\le x\le M)
\because\phi[[1..n]]=U
\implies\exist m,M\in U\forall x\in U.(m\le x\le M)
\iff (U,\le)には最大元と最小元が存在する
有界性を示そうとしただけだったのだが、本題が求まってしまったtakker
まあいいや